λ cube
ラムダ・キューブ - Wikipedia
Lambda cube - Wikipedia
λ計算
ラムダ計算 - Wikipedia
單純型附きλ計算
(simply-typed lambda calculus)
$ \lambda\to
項に依存した項。一階命題論理
型付きラムダ計算 - Wikipedia
Typed lambda calculus - Wikipedia
lambda-calculus in nLab
三軸
多相型
(polymorphism)
$ \lambda 2
型に依存した項
ポリモーフィズム - Wikipedia
polymorphism in nLab
Second-order propositional logic - Wikipedia
parametric 多相
Parametric polymorphism - Wikipedia
型理論 :
System F
論理 : 二階命題論理
型演算
(type operators)
$ \lambda\underline\omega
型に依存した型
型理論 :
代數的 data 型 (ADT)
論理 : 弱高階命題論理
一階述語論理 - Wikipedia#:~:text=弱二階述語論理
依存型
(dependent type)
$ \lambda\Pi
項に依存した型
依存型 - Wikipedia
Dependent type - Wikipedia
Lambda cube - Wikipedia#(λP)_Lambda-P
Logical framework - Wikipedia#LF
dependent type theory in nLab
型理論 :
直觀主義型理論
論理 :
一階述語論理 (FOL)
dependent type theory with type variables in nLab
$ \lambda\Pi 2
三軸全てを備へた
calculus of constructions (CoC)
$ \lambda C
Calculus of constructions - Wikipedia
calculus of constructions in nLab
論理 :
高階述語論理